Inference at * 
Iof proof for Lemma p-mu-decider:


  A:Type, P:(A). (x:A. Dec(n:. ((P(x,n)))))  (x:A. y: + Top. p-mu(P(x);y)) 

latex

 by (Auto) 
CollapseTHEN ((BLemma `p-mu-exists`) 
CollapseTHEN (Auto)) 

latex

C.

Definitions	Type, , x:AB(x), p-mu(P;x), left + right, Top, P  Q, f(a), t  T, Dec(P), x:A. B(x), x:A  B(x), b, , x:A. B(x)
Lemmas	p-mu-exists